{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## algorithm"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "class Unify:\n",
    "    \n",
    "    def __init__(self):\n",
    "        self.reference = {}   # variable bindings\n",
    "        self.checkpoint = []  # unification checkpoints\n",
    "        self.var_ctx = 0      # unique variable id\n",
    "\n",
    "    def variable(self, *args):\n",
    "        self.var_ctx += 1\n",
    "        return ['%s_%d' % (var, self.var_ctx) for var in args]\n",
    "\n",
    "    def __call__(self, var_x, var_y):\n",
    "        # resolve variable X\n",
    "        while isinstance(var_x, str) and var_x in self.reference:\n",
    "            var_x = self.reference[var_x]\n",
    "\n",
    "        # resolve variable Y\n",
    "        while isinstance(var_y, str) and var_y in self.reference:\n",
    "            var_y = self.reference[var_y]\n",
    "\n",
    "        # unified to self?\n",
    "        if isinstance(var_x, str) and isinstance(var_y, str):\n",
    "            if var_x == var_y:\n",
    "                return True\n",
    "\n",
    "        # unify free variable X\n",
    "        if isinstance(var_x, str):\n",
    "            self.reference[var_x] = var_y\n",
    "            self.checkpoint[-1].append(var_x)\n",
    "            return True\n",
    "\n",
    "        # unify free variable Y\n",
    "        if isinstance(var_y, str):\n",
    "            self.reference[var_y] = var_x\n",
    "            self.checkpoint[-1].append(var_y)\n",
    "            return True\n",
    "\n",
    "        # tuple is unified element-wise\n",
    "        if isinstance(var_x, tuple) and isinstance(var_y, tuple):\n",
    "            if len(var_x) == len(var_y):\n",
    "                return all(self(i, j) for i, j in zip(var_x, var_y))\n",
    "\n",
    "        # atom is unified on equality\n",
    "        if isinstance(var_x, int) and isinstance(var_y, int):\n",
    "            if var_x == var_y:\n",
    "                return True\n",
    "\n",
    "        # not unifiable\n",
    "        raise KeyError()\n",
    "\n",
    "    def __getitem__(self, var):\n",
    "        # resolve tuple by members\n",
    "        if isinstance(var, tuple):\n",
    "            return tuple(self[i] for i in var)\n",
    "\n",
    "        # resolve variable recursively\n",
    "        if isinstance(var, str):\n",
    "            if var in self.reference:\n",
    "                return self[self.reference[var]]\n",
    "            return var\n",
    "\n",
    "        # atomic value\n",
    "        if isinstance(var, int):\n",
    "            return var\n",
    "\n",
    "        # invalid object\n",
    "        raise TypeError()\n",
    "\n",
    "    def __enter__(self):\n",
    "        # store unification checkpoint\n",
    "        self.checkpoint.append([])\n",
    "\n",
    "    def __exit__(self, exc_type, *args):\n",
    "        # remove checkpoint and unbind variables\n",
    "        for var in self.checkpoint.pop():\n",
    "            if var in self.reference:\n",
    "                del self.reference[var]\n",
    "\n",
    "        # suppress exception\n",
    "        if exc_type is not GeneratorExit:\n",
    "            return True"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "def conc(PREFIX, SUFFIX, RESULT):\n",
    "    HEAD, TAIL, CONC = unify.variable('HEAD', 'TAIL', 'CONC')\n",
    "\n",
    "    with unify:\n",
    "        unify(PREFIX, EMPTY) and unify(SUFFIX, RESULT)\n",
    "        yield\n",
    "\n",
    "    with unify:\n",
    "        unify(PREFIX, (HEAD, TAIL)) and unify(RESULT, (HEAD, CONC))\n",
    "        yield from conc(TAIL, SUFFIX, CONC)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## run"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "unify = Unify()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "EMPTY = tuple()\n",
    "prefix = (1, (2, EMPTY))\n",
    "suffix = (3, (4, EMPTY))\n",
    "result = (1, (2, (3, (4, EMPTY))))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### concatenate PREFIX and SUFFIX"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(1, (2, (3, (4, ()))))\n"
     ]
    }
   ],
   "source": [
    "for _ in conc(prefix, suffix, 'RESULT'):\n",
    "    print(unify['RESULT'])"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### what was concatenated to PREFIX if RESULT is this?"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(3, (4, ()))\n"
     ]
    }
   ],
   "source": [
    "for _ in conc(prefix, 'SUFFIX', result):\n",
    "    print(unify['SUFFIX'])"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### this is super cool! if RESULT is this, what was PREFIX and SUFFIX?"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "possible answer is () and (1, (2, (3, (4, ()))))\n",
      "possible answer is (1, ()) and (2, (3, (4, ())))\n",
      "possible answer is (1, (2, ())) and (3, (4, ()))\n",
      "possible answer is (1, (2, (3, ()))) and (4, ())\n",
      "possible answer is (1, (2, (3, (4, ())))) and ()\n"
     ]
    }
   ],
   "source": [
    "for _ in conc('PREFIX', 'SUFFIX', result):\n",
    "    print('possible answer is', unify['PREFIX'], 'and', unify['SUFFIX'])"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### if PREFIX and SUFFIX are concatenated, would this be RESULT?"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "yes\n"
     ]
    }
   ],
   "source": [
    "for _ in conc(prefix, suffix, result):\n",
    "    print('yes')\n",
    "    break\n",
    "else:\n",
    "    print('no')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "yes\n"
     ]
    }
   ],
   "source": [
    "for _ in conc(prefix, suffix, result):\n",
    "    print('yes')\n",
    "    break\n",
    "else:\n",
    "    print('no')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## most people won't solve this one"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "PREFIX = ()\n",
      "SUFFIX = RESULT\n",
      "RESULT = RESULT\n",
      "\n",
      "PREFIX = ('HEAD_18', ())\n",
      "SUFFIX = CONC_18\n",
      "RESULT = ('HEAD_18', 'CONC_18')\n",
      "\n",
      "PREFIX = ('HEAD_18', ('HEAD_19', ()))\n",
      "SUFFIX = CONC_19\n",
      "RESULT = ('HEAD_18', ('HEAD_19', 'CONC_19'))\n",
      "\n",
      "PREFIX = ('HEAD_18', ('HEAD_19', ('HEAD_20', ())))\n",
      "SUFFIX = CONC_20\n",
      "RESULT = ('HEAD_18', ('HEAD_19', ('HEAD_20', 'CONC_20')))\n",
      "\n",
      "PREFIX = ('HEAD_18', ('HEAD_19', ('HEAD_20', ('HEAD_21', ()))))\n",
      "SUFFIX = CONC_21\n",
      "RESULT = ('HEAD_18', ('HEAD_19', ('HEAD_20', ('HEAD_21', 'CONC_21'))))\n",
      "\n"
     ]
    }
   ],
   "source": [
    "for _ in zip(range(5), conc('PREFIX', 'SUFFIX', 'RESULT')):\n",
    "    print('PREFIX =', unify['PREFIX'])\n",
    "    print('SUFFIX =', unify['SUFFIX'])\n",
    "    print('RESULT =', unify['RESULT'])\n",
    "    print()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.6.0"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}
